Konig(k)
== tree:((n:  ({0..n}{0..k}))).
== (i, j:. (i  j)  (x:({0..j}{0..k}). ((tree(<j, x>)))  ((tree(<i, x>)))))
==  ((b:. (x:({0..b}{0..k}). ((tree(<b, x>))))))
==  (s:{0..k}. (n:. (tree(<n, s>)))) 

latex

---

clarification:

Konig(k)
== tree:((n:  ({0..n}{0..k}))).
== (i:, j:. (i  j)  (x:({0..j}{0..k}). ((tree(<j, x>)))  ((tree(<i, x>)))))
==  ((b:. (x:({0..b}{0..k}). ((tree(<b, x>))))))
==  (s:{0..k}. (n:. (tree(<n, s>)))) 

latex

Definitions	x:A  B(x), , A  B, P  Q, A, x:A. B(x), x:AB(x), {i..j}, #$n, x:A. B(x), , b, f(a), <a, b>
FDL editor aliases	Konig